Nuprl Lemma : exp_unroll_q
11,40
postcript
pdf
n
:
,
e
:
.
e
n
= (
e
n
- 1 *
e
)
latex
Definitions
t
T
,
t
.2
,
t
.1
,
CRng
,
<
+*>
,
*
,
x
f
y
,
|
r
|
,
x
:
A
.
B
(
x
)
,
r
n
Lemmas
crng
wf
,
qrng
wf
,
rng
nexp
unroll
origin
n:
, e:
. e 
n = (e n - 1 * e) 
n:, e:. e n = (e n - 1 * e) T+*>x:A. B(x) n